Issue5363b.agda:8,17-18
Variable a is declared erased, so it cannot be used here
when checking that the expression a has type Level
